T:Type, as, bs:T List.
no_repeats(T;as)
 no_repeats(T;bs)
 (as = bs  (x:T. (x  as)  (x  bs)) & (x, y:T. x before y  as  x before y  bs)) 

latex

Definitions

x:A. B(x), t  T, x before y  l, (x  l), Type, no_repeats(T;l), P  Q, x:AB(x), Prop, x:AB(x), P & Q, P  Q, P  Q, type List, s = t, car.cdr, nil, tl(l), n-m, if a<b c ; d fi, i<j, b, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), x.A(x), Y, ||as||, a<b, A, AB, , {x:A| B(x) }, , False, {T}, P  Q, left+right, x. t(x), True, T

Lemmas

squash wf, true wf, l before member2, l before member, no repeats cons, all functionality wrt iff, iff functionality wrt iff, cons before, cons member, nil member, iff wf, no repeats wf, l member wf, l before wf